$\forall$$A$:Type, ${\it eq}$:EqDecider($A$), $x$:$A$, $v$,$z$:top. sqequal(fpf{-}cap(fpf{-}single($x$; $v$); ${\it eq}$; $x$; $z$); $v$)